YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Weak Trs: { #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add following dependency tuples: Strict DPs: { #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , findMin^#(@l) -> c_2(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , findMin#1^#(nil()) -> c_4() , findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , findMin#2^#(nil(), @x) -> c_6() , findMin#3^#(#false(), @x, @y, @ys) -> c_7() , findMin#3^#(#true(), @x, @y, @ys) -> c_8() , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) , minSort#1^#(nil()) -> c_11() } Weak DPs: { #cklt^#(#EQ()) -> c_24() , #cklt^#(#GT()) -> c_25() , #cklt^#(#LT()) -> c_26() , #compare^#(#0(), #0()) -> c_12() , #compare^#(#0(), #neg(@y)) -> c_13() , #compare^#(#0(), #pos(@y)) -> c_14() , #compare^#(#0(), #s(@y)) -> c_15() , #compare^#(#neg(@x), #0()) -> c_16() , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_18() , #compare^#(#pos(@x), #0()) -> c_19() , #compare^#(#pos(@x), #neg(@y)) -> c_20() , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_22() , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , findMin^#(@l) -> c_2(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , findMin#1^#(nil()) -> c_4() , findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , findMin#2^#(nil(), @x) -> c_6() , findMin#3^#(#false(), @x, @y, @ys) -> c_7() , findMin#3^#(#true(), @x, @y, @ys) -> c_8() , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) , minSort#1^#(nil()) -> c_11() } Weak DPs: { #cklt^#(#EQ()) -> c_24() , #cklt^#(#GT()) -> c_25() , #cklt^#(#LT()) -> c_26() , #compare^#(#0(), #0()) -> c_12() , #compare^#(#0(), #neg(@y)) -> c_13() , #compare^#(#0(), #pos(@y)) -> c_14() , #compare^#(#0(), #s(@y)) -> c_15() , #compare^#(#neg(@x), #0()) -> c_16() , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_18() , #compare^#(#pos(@x), #0()) -> c_19() , #compare^#(#pos(@x), #neg(@y)) -> c_20() , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_22() , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,4,6,7,8,11} by applications of Pre({1,4,6,7,8,11}) = {2,3,5,9}. Here rules are labeled as follows: DPs: { 1: #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 2: findMin^#(@l) -> c_2(findMin#1^#(@l)) , 3: findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , 4: findMin#1^#(nil()) -> c_4() , 5: findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , 6: findMin#2^#(nil(), @x) -> c_6() , 7: findMin#3^#(#false(), @x, @y, @ys) -> c_7() , 8: findMin#3^#(#true(), @x, @y, @ys) -> c_8() , 9: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , 10: minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) , 11: minSort#1^#(nil()) -> c_11() , 12: #cklt^#(#EQ()) -> c_24() , 13: #cklt^#(#GT()) -> c_25() , 14: #cklt^#(#LT()) -> c_26() , 15: #compare^#(#0(), #0()) -> c_12() , 16: #compare^#(#0(), #neg(@y)) -> c_13() , 17: #compare^#(#0(), #pos(@y)) -> c_14() , 18: #compare^#(#0(), #s(@y)) -> c_15() , 19: #compare^#(#neg(@x), #0()) -> c_16() , 20: #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , 21: #compare^#(#neg(@x), #pos(@y)) -> c_18() , 22: #compare^#(#pos(@x), #0()) -> c_19() , 23: #compare^#(#pos(@x), #neg(@y)) -> c_20() , 24: #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , 25: #compare^#(#s(@x), #0()) -> c_22() , 26: #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { findMin^#(@l) -> c_2(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) } Weak DPs: { #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #cklt^#(#EQ()) -> c_24() , #cklt^#(#GT()) -> c_25() , #cklt^#(#LT()) -> c_26() , #compare^#(#0(), #0()) -> c_12() , #compare^#(#0(), #neg(@y)) -> c_13() , #compare^#(#0(), #pos(@y)) -> c_14() , #compare^#(#0(), #s(@y)) -> c_15() , #compare^#(#neg(@x), #0()) -> c_16() , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_18() , #compare^#(#pos(@x), #0()) -> c_19() , #compare^#(#pos(@x), #neg(@y)) -> c_20() , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_22() , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) , findMin#1^#(nil()) -> c_4() , findMin#2^#(nil(), @x) -> c_6() , findMin#3^#(#false(), @x, @y, @ys) -> c_7() , findMin#3^#(#true(), @x, @y, @ys) -> c_8() , minSort#1^#(nil()) -> c_11() } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {3} by applications of Pre({3}) = {2}. Here rules are labeled as follows: DPs: { 1: findMin^#(@l) -> c_2(findMin#1^#(@l)) , 2: findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , 3: findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , 4: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , 5: minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) , 6: #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 7: #cklt^#(#EQ()) -> c_24() , 8: #cklt^#(#GT()) -> c_25() , 9: #cklt^#(#LT()) -> c_26() , 10: #compare^#(#0(), #0()) -> c_12() , 11: #compare^#(#0(), #neg(@y)) -> c_13() , 12: #compare^#(#0(), #pos(@y)) -> c_14() , 13: #compare^#(#0(), #s(@y)) -> c_15() , 14: #compare^#(#neg(@x), #0()) -> c_16() , 15: #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , 16: #compare^#(#neg(@x), #pos(@y)) -> c_18() , 17: #compare^#(#pos(@x), #0()) -> c_19() , 18: #compare^#(#pos(@x), #neg(@y)) -> c_20() , 19: #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , 20: #compare^#(#s(@x), #0()) -> c_22() , 21: #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) , 22: findMin#1^#(nil()) -> c_4() , 23: findMin#2^#(nil(), @x) -> c_6() , 24: findMin#3^#(#false(), @x, @y, @ys) -> c_7() , 25: findMin#3^#(#true(), @x, @y, @ys) -> c_8() , 26: minSort#1^#(nil()) -> c_11() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { findMin^#(@l) -> c_2(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) } Weak DPs: { #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #cklt^#(#EQ()) -> c_24() , #cklt^#(#GT()) -> c_25() , #cklt^#(#LT()) -> c_26() , #compare^#(#0(), #0()) -> c_12() , #compare^#(#0(), #neg(@y)) -> c_13() , #compare^#(#0(), #pos(@y)) -> c_14() , #compare^#(#0(), #s(@y)) -> c_15() , #compare^#(#neg(@x), #0()) -> c_16() , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_18() , #compare^#(#pos(@x), #0()) -> c_19() , #compare^#(#pos(@x), #neg(@y)) -> c_20() , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_22() , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) , findMin#1^#(nil()) -> c_4() , findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , findMin#2^#(nil(), @x) -> c_6() , findMin#3^#(#false(), @x, @y, @ys) -> c_7() , findMin#3^#(#true(), @x, @y, @ys) -> c_8() , minSort#1^#(nil()) -> c_11() } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #less^#(@x, @y) -> c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #cklt^#(#EQ()) -> c_24() , #cklt^#(#GT()) -> c_25() , #cklt^#(#LT()) -> c_26() , #compare^#(#0(), #0()) -> c_12() , #compare^#(#0(), #neg(@y)) -> c_13() , #compare^#(#0(), #pos(@y)) -> c_14() , #compare^#(#0(), #s(@y)) -> c_15() , #compare^#(#neg(@x), #0()) -> c_16() , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_18() , #compare^#(#pos(@x), #0()) -> c_19() , #compare^#(#pos(@x), #neg(@y)) -> c_20() , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_22() , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) , findMin#1^#(nil()) -> c_4() , findMin#2^#(::(@y, @ys), @x) -> c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) , findMin#2^#(nil(), @x) -> c_6() , findMin#3^#(#false(), @x, @y, @ys) -> c_7() , findMin#3^#(#true(), @x, @y, @ys) -> c_8() , minSort#1^#(nil()) -> c_11() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { findMin^#(@l) -> c_2(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { findMin#1^#(::(@x, @xs)) -> c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { findMin^#(@l) -> c_1(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { findMin^#(@l) -> c_1(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 2: findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) , 3: minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#less](x1, x2) = [1] [1] [#compare](x1, x2) = [1 1] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] [#cklt](x1) = [1] [1] [findMin](x1) = [1 0] x1 + [0] [0 1] [0] [findMin#1](x1) = [1 0] x1 + [0] [0 1] [0] [::](x1, x2) = [1 1] x2 + [1] [0 1] [1] [findMin#2](x1, x2) = [1 1] x1 + [1] [0 1] [1] [nil] = [0] [0] [findMin#3](x1, x2, x3, x4) = [2 1] x1 + [1 2] x4 + [0] [1 0] [0 1] [1] [#false] = [1] [1] [#true] = [1] [1] [#EQ] = [2] [2] [#GT] = [0] [1] [#LT] = [0] [0] [#0] = [0] [0] [#neg](x1) = [1 0] x1 + [0] [0 1] [0] [#pos](x1) = [1 0] x1 + [0] [0 1] [0] [#s](x1) = [1 0] x1 + [0] [0 1] [0] [#less^#](x1, x2) = [0] [0] [#cklt^#](x1) = [0] [0] [#compare^#](x1, x2) = [0] [0] [findMin^#](x1) = [0 1] x1 + [0] [0 0] [0] [findMin#1^#](x1) = [0 1] x1 + [0] [0 0] [1] [findMin#2^#](x1, x2) = [0] [0] [findMin#3^#](x1, x2, x3, x4) = [0] [0] [minSort^#](x1) = [2 1] x1 + [2] [0 1] [0] [minSort#1^#](x1) = [2 0] x1 + [0] [1 0] [0] [c_1](x1) = [1 0] x1 + [0] [0 0] [0] [c_2](x1) = [1 1] x1 + [0] [0 0] [0] [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_4](x1) = [1 0] x1 + [0] [0 0] [0] This order satisfies following ordering constraints [#less(@x, @y)] = [1] [1] >= [1] [1] = [#cklt(#compare(@x, @y))] [#cklt(#EQ())] = [1] [1] >= [1] [1] = [#false()] [#cklt(#GT())] = [1] [1] >= [1] [1] = [#false()] [#cklt(#LT())] = [1] [1] >= [1] [1] = [#true()] [findMin(@l)] = [1 0] @l + [0] [0 1] [0] >= [1 0] @l + [0] [0 1] [0] = [findMin#1(@l)] [findMin#1(::(@x, @xs))] = [1 1] @xs + [1] [0 1] [1] >= [1 1] @xs + [1] [0 1] [1] = [findMin#2(findMin(@xs), @x)] [findMin#1(nil())] = [0] [0] >= [0] [0] = [nil()] [findMin#2(::(@y, @ys), @x)] = [1 2] @ys + [3] [0 1] [2] >= [1 2] @ys + [3] [0 1] [2] = [findMin#3(#less(@x, @y), @x, @y, @ys)] [findMin#2(nil(), @x)] = [1] [1] >= [1] [1] = [::(@x, nil())] [findMin#3(#false(), @x, @y, @ys)] = [1 2] @ys + [3] [0 1] [2] >= [1 2] @ys + [3] [0 1] [2] = [::(@y, ::(@x, @ys))] [findMin#3(#true(), @x, @y, @ys)] = [1 2] @ys + [3] [0 1] [2] >= [1 2] @ys + [3] [0 1] [2] = [::(@x, ::(@y, @ys))] [findMin^#(@l)] = [0 1] @l + [0] [0 0] [0] >= [0 1] @l + [0] [0 0] [0] = [c_1(findMin#1^#(@l))] [findMin#1^#(::(@x, @xs))] = [0 1] @xs + [1] [0 0] [1] > [0 1] @xs + [0] [0 0] [0] = [c_2(findMin^#(@xs))] [minSort^#(@l)] = [2 1] @l + [2] [0 1] [0] > [2 1] @l + [0] [0 0] [0] = [c_3(minSort#1^#(findMin(@l)), findMin^#(@l))] [minSort#1^#(::(@x, @xs))] = [2 2] @xs + [2] [1 1] [1] >= [2 1] @xs + [2] [0 0] [0] = [c_4(minSort^#(@xs))] Consider the set of all dependency pairs DPs: { 1: findMin^#(@l) -> c_1(findMin#1^#(@l)) , 2: findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) , 3: minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l)) , 4: minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) } Processor 'matrix interpretation of dimension 2' induces the complexity certificate YES(?,O(n^2)) on application of dependency pairs {2,3}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { findMin^#(@l) -> c_1(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) } Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { findMin^#(@l) -> c_1(findMin#1^#(@l)) , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l)) , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 2.353892s CPU-time: 17.456s Hurray, we answered YES(O(1),O(n^2))